package tp;

import java.io.Serializable;
import java.util.ArrayList;
import java.util.HashSet;

import randoop.CheckRep;

import korat.finitization.IClassDomain;
import korat.finitization.IFinitization;
import korat.finitization.IObjSet;
import korat.finitization.impl.FinitizationFactory;

/**
 * Implementacion del TAD Lista, usando una estructura dinámica, más
 * precisamente un árbol binario de búsqueda. Esta clase implementa los métodos
 * abstractos declarados en List, y corresponde a una implementación
 * polimórfica.
 * 
 * @author Nazareno Aguirre, Valeria Bengolea & Renzo Degiovanni
 * @version 0.1 22/04/2013
 */
public class TreeList implements List, Serializable {

	private static final long serialVersionUID = 1L;

	private Node root; // tree that stores list' elements

	private int size; // number of elements in the list

	public TreeList() {
		root = null;
		size = 0;
	}

	public boolean isEmpty() {
		return size == 0;
	}

	public int size() {
		return size;
	}

	/*--------------------------------------------------------------------*/
	/* removeAll(): removes all the items from the list */
	/* Precondition: None */
	/* Postcondition: all elements are removed from the list. */
	/*--------------------------------------------------------------------*/
	public void removeAll() {
		root = null;
		size = 0;
	}

	/*--------------------------------------------------------------------*/
	/* add(int index, Object item ): adds item to the list in position */
	/* index */
	/*--------------------------------------------------------------------*/
	public void add(int index, Object item) throws RuntimeException,
			IndexOutOfBoundsException {
		if (item == null)
			throw new RuntimeException("attempting to insert null object");
		if (index < 0 || index > size)
			throw new IndexOutOfBoundsException(
					"index out of bounds in tree list");

		// agrega el nodo al arbol en la posicion index
		// y retorna la referencia al mismo
		Node recentlyAdded = add(root, index, item);
		size++;
		// incremento los debidos indices del arbol
		Utils.correctIndexes(root, recentlyAdded, index, 1);
	}

	/**
	 * @param node
	 * @param index
	 * @param item
	 * @return referencia al nodo del arbol insertado en la posicion index
	 */
	private Node add(Node node, int index, Object item) {
		if (node == null && index == 0)
			return (root = new Node(index, item));
		if (index == size) {
			Node newNode = new Node(index, item);
			Utils.getMax(node).setRight(newNode);
			return newNode;
		}
		if (node.getIndex() == index) {
			// creo un nuevo nodo con el mismo campo index e info
			// que el que tenia el indice index en la lista
			Node oldNode = new Node(index, node.getInfo());

			// si root.getRight() != null, busco el menor de sus hijos
			if (node.getRight() != null)
				Utils.getMin(node.getRight()).setLeft(oldNode);
			else
				// como root.getRight == null, seteo dicho campo con el
				// nuevo nodo
				node.setRight(oldNode);

			// seteo el campo info de root
			node.setInfo(item);
			return node;
		}
		if (node.getIndex() > index)
			return add(node.getLeft(), index, item);
		else
			return add(node.getRight(), index, item);
	}

	/*--------------------------------------------------------------------*/
	/* remove(int index): removes item in the index position of the list */
	/*--------------------------------------------------------------------*/
	public void remove(int index) throws IndexOutOfBoundsException {
		if (index < 0 || index >= size)
			throw new IndexOutOfBoundsException(
					"index out of bounds in tree list");

		// elimino el nodo que tiene indice index
		remove(null, root, index, true);
		size--;
		// decremento los debidos indices del arbol
		Utils.correctIndexes(root, null, index, -1);
	}

	/**
	 * @param previousNode
	 *            : referencia al nodo padre de node (en la primer llamada a
	 *            este metodo, previousNode == null).
	 * @param node
	 *            : referencia al nodo a borrar.
	 * @param index
	 *            : indice del nodo a borrar.
	 * @param isLeft
	 *            : true ssi node es hijo izquierdo de previousNode (en la
	 *            primer llamada a este metodo, isLeft == true, ya que si
	 *            previousNode == null no importan los valores de isLeft, ya que
	 *            node == root)
	 * 
	 *            Dado un nodo (node), el padre de ese nodo (previousNode),
	 *            elimina node del arbol, y en caso de ser necesario, modifica
	 *            las referencias de previousNode para mantener la consistencia
	 *            en la estructura del arbol
	 */
	private void remove(Node previousNode, Node node, int index, boolean isLeft) {
		if (node.getIndex() == index) {
			if (node.getRight() != null) // node tiene hijo derecho
				Utils.exchange(node, Utils.getMin(node.getRight()),
						node.getRight(), true);
			else if (node.getLeft() != null) // node tiene hijo izquierdo
				Utils.exchange(node, Utils.getMax(node.getLeft()),
						node.getLeft(), false);
			else // node es una hoja
			if (node == root) // si lo que se quiere eliminar es la raiz de todo
								// el arbol
				root = null;
			else { // es una hoja que no es la raiz del arbol
				if (isLeft)
					previousNode.setLeft(null);
				else
					previousNode.setRight(null);
			}
			return;
		}
		if (node.getIndex() > index)
			remove(node, node.getLeft(), index, true);
		else
			remove(node, node.getRight(), index, false);
	}

	/*--------------------------------------------------------------------*/
	/* get(int index): returns the reference to the object in position */
	/* index */
	/*--------------------------------------------------------------------*/
	public Object get(int index) throws IndexOutOfBoundsException {
		if (index < 0 || index >= size)
			throw new IndexOutOfBoundsException(
					"index out of bounds in tree list");

		return get(root, index);
	}

	/**
	 * @param root
	 * @param index
	 * @return la referencia al nodo de indice index
	 */
	private Object get(Node root, int index) {
		if (root.getIndex() == index)
			return root.getInfo();
		if (root.getIndex() > index)
			return get(root.getLeft(), index);
		else
			return get(root.getRight(), index);
	}

	/**
	 * invariante de representación de la estructura.
	 * 
	 * @return true si y sólo si la estructura es internamente consistente
	 * @pre. true
	 * @post. Se retorna true si y sólo si root aloja un árbol binario de
	 *        búsqueda (respecto a index), todos los elementos del árbol son no
	 *        nulos (respecto a info), size se corresponde con el número de
	 *        nodos del árbol, y las claves del árbol son 0..size-1.
	 */
	@CheckRep
	public boolean repOK() {
		HashSet<Node> set = new HashSet<Node>();
		// check if the tree is empty then its size is zero.
		if (root == null)
			return size == 0;
		if (!Utils.isAciclyc(root, set) // check if my tree has no cycles.
				|| (size != set.size()) // check that all my nodes belong to the tree
				|| (!Utils.nodesWithDataAndIndex(root, size))// check if all the nodes of the tree have data.
				|| (!Utils.isBinarySearchTree(root))) // check if binary search tree.
			return false;
		return true;
	}

	public String toString() {
		String result = "";
		ArrayList<Node> list = new ArrayList<Node>();
		Utils.inOrder(root, list);
		for (Node node : list) {
			result += node.toString() + " ";
		}
		return result;
	}

	/**
	 * @param numberOfValues
	 * @param minValue
	 * @param maxValue
	 * @param valueOfNodes
	 * @return IFinitization
	 */
	public static IFinitization finTreeList(int maxValue) {
		IFinitization fin = FinitizationFactory.create(TreeList.class);
		IObjSet nodes = fin.createObjSet(Node.class, maxValue, true);
		IObjSet dataValues = fin.createObjSet(Integer.class);
		
		IClassDomain domain = fin.createClassDomain(Integer.class);
		domain.includeInIsomorphismCheck(false);
		domain.addObject(new Integer(0));
		
		dataValues.addClassDomain(domain);
		dataValues.setNullAllowed(false);
		
		fin.set("root", nodes);
		fin.set("size", fin.createIntSet(0, maxValue));
		fin.set("Node.info", dataValues);
		fin.set("Node.index", fin.createIntSet(0, maxValue - 1));
		fin.set("Node.left", nodes);
		fin.set("Node.right", nodes);
		return fin;
	}
}